\begin{tabbing}
$\forall$\=$i$:Id, $k$:Knd, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:${\it ltg}$:Knd fp$\rightarrow$ Type,\+
\\[0ex]$f$:(${\it tg}$:Id$\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$(${\it da}$(rcv($l$,${\it tg}$))?Void List))) List.
\-\\[0ex]@$i$: with declarations ds:${\it ds}$da:${\it da}$ $k$(v) sends $f$ s v on link $l$ $\in$ Dsys
\end{tabbing}